(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 1))
(let ((e4 3))
(let ((e5 4))
(let ((e6 (- v1)))
(let ((e7 (- v2)))
(let ((e8 (* e6 e6)))
(let ((e9 (- v0)))
(let ((e10 (- v2)))
(let ((e11 (* e6 v2)))
(let ((e12 (* e10 e8)))
(let ((e13 (+ e7 v0)))
(let ((e14 (/ e3 e3)))
(let ((e15 (/ e4 e5)))
(let ((e16 (< v1 e6)))
(let ((e17 (>= e12 e14)))
(let ((e18 (distinct e12 e15)))
(let ((e19 (> e8 e13)))
(let ((e20 (distinct e8 e11)))
(let ((e21 (> v1 e9)))
(let ((e22 (< v0 v0)))
(let ((e23 (= v1 e9)))
(let ((e24 (< e7 e8)))
(let ((e25 (< e15 e10)))
(let ((e26 (< e10 e12)))
(let ((e27 (< v1 e15)))
(let ((e28 (>= e7 e6)))
(let ((e29 (>= e12 v0)))
(let ((e30 (= v2 v2)))
(let ((e31 (distinct e11 v1)))
(let ((e32 (<= v2 v1)))
(let ((e33 (> v0 e10)))
(let ((e34 (< e15 v1)))
(let ((e35 (<= e14 e11)))
(let ((e36 (< e6 v2)))
(let ((e37 (= e15 e8)))
(let ((e38 (<= e8 v1)))
(let ((e39 (> e7 e11)))
(let ((e40 (distinct e15 e13)))
(let ((e41 (>= v2 e12)))
(let ((e42 (<= e6 v0)))
(let ((e43 (< e10 e10)))
(let ((e44 (distinct e14 e8)))
(let ((e45 (< e12 e15)))
(let ((e46 (= e9 e10)))
(let ((e47 (or e20 e20)))
(let ((e48 (ite e25 e24 e19)))
(let ((e49 (=> e43 e39)))
(let ((e50 (xor e16 e29)))
(let ((e51 (xor e50 e40)))
(let ((e52 (= e51 e51)))
(let ((e53 (=> e52 e48)))
(let ((e54 (not e37)))
(let ((e55 (=> e30 e45)))
(let ((e56 (not e26)))
(let ((e57 (and e36 e53)))
(let ((e58 (ite e23 e46 e55)))
(let ((e59 (and e33 e41)))
(let ((e60 (and e59 e21)))
(let ((e61 (= e35 e22)))
(let ((e62 (ite e47 e61 e49)))
(let ((e63 (= e44 e27)))
(let ((e64 (and e28 e34)))
(let ((e65 (ite e63 e64 e58)))
(let ((e66 (and e65 e17)))
(let ((e67 (=> e18 e42)))
(let ((e68 (xor e67 e32)))
(let ((e69 (xor e56 e66)))
(let ((e70 (=> e69 e60)))
(let ((e71 (or e54 e54)))
(let ((e72 (=> e62 e38)))
(let ((e73 (not e68)))
(let ((e74 (or e73 e70)))
(let ((e75 (or e71 e72)))
(let ((e76 (xor e74 e74)))
(let ((e77 (=> e75 e75)))
(let ((e78 (=> e31 e76)))
(let ((e79 (not e57)))
(let ((e80 (=> e77 e79)))
(let ((e81 (or e80 e78)))
e81
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
